T:Type, E:(TTProp), x, y:T. (EquivRel _1,_2:T. _1 E _2)  (x (E^*) y)  (x E y) 

latex

Definitions	R^*, P  Q, , R^n, EquivRel x,y:T. E(x;y), x:A. B(x), x,y. t(x;y), x f y, Prop, t  T, x:A. B(x), AB, A, False, ij, i=j, P & Q, Refl(T;x,y.E(x;y)), Unit, P  Q, , b, b, Trans x,y:T. E(x;y)
Lemmas	le wf, assert wf, not wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, nat properties, ge wf, equiv rel wf, rel exp wf, nat wf